sig Regione {}

sig Volo {
	fromRegione: one Regione,
	toRegione: one Regione
}

sig Hotel {
	inRegione: one Regione
}

sig Escursione {
	inRegione: one Regione
}

sig Giornata {
	id: one Int,
	hasVolo: lone Volo,
	hasHotel: lone Hotel,
 	hasEscursione: lone Escursione
}

sig Viaggio {
	hasGiornata: some Giornata
}{#hasGiornata > 1}

sig Utente {
	hasViaggio: set Viaggio
}

//----------------------------------------------------------------------------------------------------------------------//
//----------------------------------------------------------------------------------------------------------------------//

//Una giornata appartiene ad uno ed un solo viaggio
assert NoStessaGiornataInPiuViaggiAss {
	all g: Giornata {no v1, v2: Viaggio | v1!=v2 and g in v1.hasGiornata and g in v2.hasGiornata}
	all g: Giornata {one v: Viaggio | g in v.hasGiornata}
}

fact NoStessaGiornataInPiuViaggi {
	all g: Giornata {no v1, v2: Viaggio | v1!=v2 and g in v1.hasGiornata and g in v2.hasGiornata}
	all g: Giornata {one v: Viaggio | g in v.hasGiornata}
}
//check NoStessaGiornataInPiuViaggiAss


//---------------------------------------------------------------------------------------------------------------------//
//															ASSERT SUI VOLI 																//
//--------------------------------------------------------------------------------------------------------------------//


//Non esiste un volo che parte ed arriva dalla stessa Regione
assert NoVoloStessaRegioneAss {
	all v: Volo {no r: Regione | r in v.fromRegione and r in v.toRegione}
}

fact NoVoloStessaRegione {
	all v: Volo {no r: Regione | r in v.fromRegione and r in v.toRegione}
}

//Unicamente l'ultimo volo può ritornare nella regione d'origine
fact NoRitornoPrimeDellaFine {
	all v:Viaggio {
		one g1,g2:Giornata, r:Regione | g1 in v.hasGiornata and g2 in v.hasGiornata and g1!=g2 and
		g1.id=0 and r in g1.hasVolo.fromRegione and r in g2.hasVolo.toRegione
	}
}


//Tutti i voli del viaggio devono essere diversi
assert NoStessiVoliAss {
	all v: Viaggio {no g1,g2: Giornata, v1,v2: Volo | g1!=g2 and v1=v2 and g1 in v.hasGiornata and g2 in v.hasGiornata and v1 in g1.hasVolo and v2 in g2.hasVolo}
}

fact NoStessiVoli {
	all v: Viaggio {no g1,g2: Giornata, v1,v2: Volo | g1!=g2 and v1=v2 and g1 in v.hasGiornata and g2 in v.hasGiornata and v1 in g1.hasVolo and v2 in g2.hasVolo}
}


//La prima e l'ultima giornata hanno sicuramente un volo
//Non inserisco alcun fatto perchè è sempre verificata (per via di altri fatti)
assert VoloPrimaUltimaGiornataAss {
	all v: Viaggio {one g:Giornata | g in v.hasGiornata and g.id=0 and #g.hasVolo=1}
	all v: Viaggio {one g1:Giornata | g1 in v.hasGiornata and
		{no g2:Giornata | g2 in v.hasGiornata and g2.id>g1.id} and
		#g1.hasVolo=1
	}
}

//La regione di partenza e la regione di fine devono essere legate
assert PartenzaRitornoAss{
	all v: Viaggio 
	{
			one g1,g2 :Giornata | g1!=g2 and g1 in v.hasGiornata and g2 in v.hasGiornata and g1.id=0 and 
			{
					no g3:Giornata | g3 in v.hasGiornata and g3.id>g2.id
			} 
			and 
			{
					one v1,v2: Volo | v1 in g1.hasVolo and v2 in g2.hasVolo and
					{
							one r:Regione| r in v1.fromRegione and r in v2.toRegione
					}
			}
	}
}

fact PartenzaRitorno{
	all v: Viaggio 
	{
			one g1,g2 :Giornata | g1!=g2 and g1 in v.hasGiornata and g2 in v.hasGiornata and g1.id=0 and 
			{
					no g3:Giornata | g3 in v.hasGiornata and g3.id>g2.id
			} 
			and 
			{
					one v1,v2: Volo | v1 in g1.hasVolo and v2 in g2.hasVolo and
					{
							one r:Regione| r in v1.fromRegione and r in v2.toRegione
					}
			}
	}
}


//I Voli devono essere concatenati: 
//la regione di partenza di un volo deve coincidere con la regione di arrivo del volo precedente.

assert VoliConcatenatiAss {
	all v:Viaggio 
	{
		all g1:Giornata | (g1 in v.hasGiornata and g1.id!=0 and #g1.hasVolo=1) =>
		{
			some g2:Giornata | g2 in v.hasGiornata and g1.id>g2.id and
			{no g3:Giornata | g3 in v.hasGiornata and #g3.hasVolo=1 and g3.id>g2.id and g3.id<g1.id} and
			{
				one v1,v2:Volo | v1 in g1.hasVolo and v2 in g2.hasVolo and 
				{one r:Regione | r in v1.fromRegione and r in v2.toRegione}
			}
		}
	}
}

fact VoliConcatenati {
	all v: Viaggio 
	{
		all g1:Giornata | (g1 in v.hasGiornata and g1.id!=0 and #g1.hasVolo=1) =>
		{
			some g2:Giornata | g2 in v.hasGiornata and g1.id>g2.id and
			{no g3:Giornata | g3 in v.hasGiornata and #g3.hasVolo=1 and g3.id>g2.id and g3.id<g1.id} and
			{
				one v1,v2:Volo | v1 in g1.hasVolo and v2 in g2.hasVolo and 
				{one r:Regione | r in v1.fromRegione and r in v2.toRegione}
			}
		}
	}
}

//con i fatti precedenti deve anche risultare che in un qualsiasi viaggio ci debbano necessariamente essere almeno due voli
assert DueVoliAss {
	all v: Viaggio {#v.hasGiornata.hasVolo > 1}
}

//check NoStessiVoliAss 
//check NoVoloStessaRegioneAss 
//check DueVoliAss
//check VoloPrimaUltimaGiornataAss
//check PartenzaRitornoAss
//check VoliConcatenatiAss
//check NoRitornoPrimaDellaFineAss




//----------------------------------------------------------------------------------------------------------------------//
//															ESCURSIONI 																	  //
//----------------------------------------------------------------------------------------------------------------------//


//Tutte le escursioni del viaggio devono essere diverse
assert NoStesseEscursioniAss {
	all v: Viaggio 
	{
		no g1,g2: Giornata, e1,e2: Escursione | g1!=g2 and e1=e2 and g1 in v.hasGiornata and g2 in v.hasGiornata and 
		e1 in g1.hasEscursione and e2 in g2.hasEscursione
	}
}
fact NoStesseEscursioni {
	all v: Viaggio 
	{
		no g1,g2: Giornata, e1,e2: Escursione | g1!=g2 and e1=e2 and g1 in v.hasGiornata and g2 in v.hasGiornata and 
		e1 in g1.hasEscursione and e2 in g2.hasEscursione
	}
}


//Le escursioni di una determinata giornata devono avere la stessa regione dell'ultimo volo effettuato
//Bisogna prestare attenzione alla possibilità di effettuare una escursione e successivamente un volo nella stessa giornata
//in questo caso sarà necessario che il volo precedente abbia la regione in comune
assert RegioneEscursioneAss{
	all v:Viaggio 
	{
		all g1:Giornata | (g1 in v.hasGiornata and #g1.hasEscursione=1) =>
		{
			some g2:Giornata | g2 in v.hasGiornata and g2.id<=g1.id and
			{no g3:Giornata | g3 in v.hasGiornata and #g3.hasVolo=1 and g3.id>g2.id and g3.id<g1.id} and
			{
				one v2:Volo | v2 in g2.hasVolo and 
				{one r:Regione | r in g1.hasEscursione.inRegione and r in v2.toRegione}
			}
		}
	}
}

fact RegioneEscursione{
	all v:Viaggio 
	{
		all g1:Giornata | (g1 in v.hasGiornata and #g1.hasEscursione=1) =>
		{
			some g2:Giornata | g2 in v.hasGiornata and g2.id<=g1.id and
			{no g3:Giornata | g3 in v.hasGiornata and #g3.hasVolo=1 and g3.id>g2.id and g3.id<g1.id} and
			{
				one v2:Volo | v2 in g2.hasVolo and 
				{one r:Regione | r in g1.hasEscursione.inRegione and r in v2.toRegione}
			}
		}
	}
}

//Non ci posso essere escursioni con la stessa regione di quella di partenza del viaggio
assert NoEscursioneRegionePartenzaAss
{
	all v:Viaggio {	no r:Regione, g:Giornata | g in v.hasGiornata and g.id=0 and r in g.hasVolo.fromRegione and r in v.hasGiornata.hasEscursione.inRegione}
}
fact NoEscursioneRegionePartenzaAss
{
	all v:Viaggio {	no r:Regione, g:Giornata | g in v.hasGiornata and g.id=0 and r in g.hasVolo.fromRegione and r in v.hasGiornata.hasEscursione.inRegione}
}

//check NoStesseEscursioniAss
//check RegioneEscursioneAss
//check NoEscursioneRegionePartenzaAss

//----------------------------------------------------------------------------------------------------------------------//
//																HOTELS	 																	  //
//----------------------------------------------------------------------------------------------------------------------//

//Esiste unicamente una giornata in un viaggio che non ha l'hotel, ma ha necessariamente un volo
assert NoHotelUltimoGiornoAss
{
	all v: Viaggio {one g: Giornata | g in v.hasGiornata and #g.hasHotel = 0}
	all v: Viaggio {one g: Giornata | g in v.hasGiornata and #g.hasHotel = 0 and #g.hasVolo = 1}
	all v: Viaggio {one g: Giornata | g in v.hasGiornata and #g.hasHotel = 0 and {no g2:Giornata | g2 in v.hasGiornata and g2.id>g.id}}
}

fact NoHotelUltimoGiorno
{
	all v: Viaggio {one g: Giornata | g in v.hasGiornata and #g.hasHotel = 0}
	all v: Viaggio {one g: Giornata | g in v.hasGiornata and #g.hasHotel = 0 and #g.hasVolo = 1}
	all v: Viaggio {one g: Giornata | g in v.hasGiornata and #g.hasHotel = 0 and {no g2:Giornata | g2 in v.hasGiornata and g2.id>g.id}}
}



//Le regioni degli hotel devono essere legate alla regione di arrivo dell'ultimo volo
assert HotelSeguonoVoliAss {
	all v:Viaggio 
	{
		all g1:Giornata | (g1 in v.hasGiornata and #g1.hasHotel=1) =>
		{
			one g2:Giornata, r:Regione | g2 in v.hasGiornata and g2.id<=g1.id and r in g2.hasVolo.toRegione and r in g1.hasHotel.inRegione and
			{
				no g3:Giornata | g3 in v.hasGiornata  and g3.id<=g1.id and g3.id>g2.id and #g3.hasVolo=1
			}
		}
	}
}

fact HotelSeguonoVoli {
	all v:Viaggio 
	{
		all g1:Giornata | (g1 in v.hasGiornata and #g1.hasHotel=1) =>
		{
			one g2:Giornata, r:Regione | g2 in v.hasGiornata and g2.id<=g1.id and r in g2.hasVolo.toRegione and r in g1.hasHotel.inRegione and
			{
				no g3:Giornata | g3 in v.hasGiornata  and g3.id<=g1.id and g3.id>g2.id and #g3.hasVolo=1
			}
		}
	}
}

//check NoHotelUltimoGiornoAss
//check HotelSeguonoVoliAss 

//----------------------------------------------------------------------------------------------------------------------//
//----------------------------------------------------------------------------------------------------------------------//




//L'ordine degli id Giornata deve partire da 0 es essere crescente in maniera ordinata (+1)
//L'ID della giornata è utile per ordinare i giorni di viaggio!
fact OrdineGiornata {
	all v: Viaggio {one g: Giornata | g in v.hasGiornata and g.id = 0}
	all g: Giornata | g.id >= 0
	all v: Viaggio {no g1,g2: Giornata | g1 in v.hasGiornata and g2 in v.hasGiornata and g1!=g2 and g1.id=g2.id}
	all v:Viaggio 
	{
		all g1:Giornata | (g1 in v.hasGiornata and g1.id!=0) =>
		{one g2:Giornata | g2 in v.hasGiornata and g2.id=add[g1.id,-1]}
	}
}





pred show () {
}
run show
